greatcfandomcom-20200214-history
OpenEd-Lab7
[ C:TaPiC ] Lab 1 Lab 2 Lab 3 Lab 4 Lab 5 Lab 6 Lab 7 Lab 8 Recursive functions and register machines What's the point? Proving programs correct can seem intractable. Can we by starting with a very simple computing device and a simple language build up programs that are correct by construction through proof? For example consider that we want to create a program / machine to add two numbers: σ(R1) = m, σ(R2) = n // program. σ(R1) = m + n Can we prove the following? σ(R1) = m, σ(R2) = n REG_1 <- R1 REG_2 <- R2 0 STOP 1 TSTZ REG_2 0 DEC REG_2 2 2 INC REG_1 1 R1 <- REG_1 σ(R1) = m + n The following definition is take from Johnstone (1987). Definition of a register machine A register machine has a sequence of registers R1, R2, . . . , each of which may at any time hold an arbitrary natural number. A program for the machine is defined by specifying a finitie number of states S0, S1. . . . , Sn , together with, for each i > 0, an instruction to be carried out whenever the machine is in state Si . (S0 is the terminal state; on reaching it, the machine 'switches itself off'.) These instruction are of two kinds: # add 1 ro register Ri , and move to state Sk # test whether Ri holds the number 0: if it does, move to state Sl otherwise subtract 1 from it and move to state Sk . A language ::= ()* ::= 0 STOP ::= | ::= INC ::= TSTZ DEC ::= REG_ ::= Empty REG_0 The following program will empty the contents of register 0. 0 STOP 1 TSTZ REG_0 0 DEC REG_0 1 Move REG_1 into REG_0 The following program will move the contents of REG_1 into REG_0 emptying the contents of RGE_1 in the process. 0 STOP 1 TSTZ REG_0 2 DEC REG_0 1 2 TSTZ REG_1 0 DEC REG_1 3 3 INC REG_0 2 Copy REG_1 into REG_0 The following program wil copy the contents of register 1 into register 0. At the end of the excution register 0 and register 1 will contain the same value. 0 STOP 1 TSTZ REG_0 2 DEC REG_0 1 2 TSTZ REG_2 3 DEC REG_2 2 3 TSTZ REG_1 5 DEC REG_1 4 4 INC REG_2 3 5 TSTZ REG_2 0 DEC REG_0 6 6 INC REG_0 7 7 INC REG_1 5 Semantics and Proofs This is the first attempt at providing a semantics for the machines described above. * The semantics for a program is a function from state to state. ** [[P'']] : Σ → Σ * A state is a function from identifiers to natural numbers. ** Σ : ''Id → N'' [[''P]] is taken as the graph of the program and contrasts with the operational semantics described below. When a program executes it will move through program states. * A program state consists of: ** a program ** a current instruction ** and the current storage state * A program state has the signature: ** PS : P'' × ''N × Σ * A program is a function from natural numbers to instructions: * P'' : ''N → I'' * An instruction is a pair of functions. ** The first function is a function from storage state to natural numbers ** The second function is a function from storage state to storage state * An instruction has the signature: ** ''I : Σ → N'' × Σ → Σ The delta function The delta function at the level of instructions is defined as follows: * Δ(''p, σ) = Δ(p'', 1, σ) * Δ(''p, n'', σ) = Δ(''p, Δ''n'',0(σ), Δ''n'',1(σ)) * Δ(p, 0, σ) = σ TODO: fuller explanation of the above. Category:OpenEd